# !/usr/bin/env python3
# -*- coding: utf-8 -*-
# @Time : 2023/4/25 14:50
# @Author : xyjiang1216
# @Email : jiangxuyan@nudt.edu.cn
# @File : window_algo_utils.py
# @Version: OpenPlanner2.0
import math
import re
import time
from typing import List

from z3 import And, Store, Or, unknown, sat, Solver, unsat, simplify

from OpenPlanner.examples.window_demo.window_algo_input import GCLLink, GCLInstance, GCLStream
from OpenPlanner.util.compute_hyper_period import compute_hyper_period


def construct_constraints(
        link_obj_set: List[GCLLink],
        stream_obj_set: List[GCLStream],
        stream_instance_obj_set: List[List[List[GCLInstance]]],
        sync_precision: int
):
    formula = []

    hyper_period = compute_hyper_period(*[int(stream_obj.period) for stream_obj in stream_obj_set])

    # 1. well-defined windows constraints
    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        stream_id_and_hop_id_set = link_obj.stream_array
        if len(stream_id_and_hop_id_set) != 0:
            phi = link_obj.phi_array[0]
            tau = link_obj.tau_array[gcl_len - 1]
            constraint_1 = And(phi >= 0, tau < hyper_period)
            # print(constraint_1)
            formula.append(constraint_1)
            # s.add(constraint_1)
    # print(formula)

    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        stream_id_and_hop_id_set = link_obj.stream_array
        if len(stream_id_and_hop_id_set) != 0:
            for k in range(gcl_len):
                kappa = link_obj.kappa_array[k]
                constraint_1 = And(kappa >= 0, kappa < link_obj.st_queues)
                formula.append(constraint_1)
                # s.add(constraint_1)
    # print(formula)

    # 2. stream instance constraints
    for instance_obj_set_per_stream in stream_instance_obj_set:
        for instance_obj_set_per_link in instance_obj_set_per_stream:
            j = 0
            for instance_obj in instance_obj_set_per_link:
                link_id = instance_obj.link_id
                stream_id = instance_obj.stream_id
                period = stream_obj_set[stream_id].period
                phi = link_obj_set[link_id].phi_array
                tau = link_obj_set[link_id].tau_array
                omega = instance_obj.omega
                constraint_2 = And(phi[omega] >= j * period,
                                   tau[omega] < (j + 1) * period)
                formula.append(constraint_2)
                # s.add(constraint_2)
                j += 1
    # print(formula)

    # 3. ordered windows constraint
    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        for i in range(gcl_len - 1):
            phi = link_obj.phi_array[i + 1]
            tau = link_obj.tau_array[i]
            constraint_3 = (tau <= phi)
            formula.append(constraint_3)
            # s.add(constraint_3)
    # print(formula)

    # 4. frame-to-window assignment constraint
    for instance_obj_set_per_stream in stream_instance_obj_set:
        for instance_obj_set_per_link in instance_obj_set_per_stream:
            for instance_obj in instance_obj_set_per_link:
                link_id = instance_obj.link_id
                gcl_len = link_obj_set[link_id].gcl_len
                omega = instance_obj.omega
                constraint_4 = And(omega >= 0, omega <= gcl_len - 1)
                formula.append(constraint_4)
                # s.add(constraint_4)
    # print(formula)

    # 5. window size constraint
    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        phi_array = link_obj.phi_array
        # 这里的tau应该是初始的tau，因此应该取T_0
        tau_0_array = link_obj.tau_0_array
        if len(link_obj.stream_array) == 0:
            continue
        for k in range(gcl_len):
            # Store(a, i, v) returns a new array identical to a,
            # but on position i it contains the value v
            # array操作无法添加到solver里面？
            # tau = Store(tau, k, phi[k])
            # T_0的值应当永远与phi保持一致
            # s.add(tau_0_array == Store(tau_0_array, k, phi_array[k]))
            constraint_5 = (tau_0_array == Store(tau_0_array, k, phi_array[k]))
            formula.append(constraint_5)
            # s.add(constraint_5)

    # 将tau_1所有元素初始化成0
    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        tau_1_array = link_obj.tau_1_array
        # tau_1 = K(IntSort(), 0)
        if len(link_obj.stream_array) == 0:
            continue
        for k in range(gcl_len):
            tau_1_array = Store(tau_1_array, k, 0)
            link_obj.tau_1_array = tau_1_array

    # 用tau_1存放中间结果
    for stream_instance_obj_set_per_stream in stream_instance_obj_set:
        hop_id = 0
        for stream_instance_obj_set_per_link in stream_instance_obj_set_per_stream:
            for stream_instance_obj in stream_instance_obj_set_per_link:
                link_id = stream_instance_obj.link_id
                tau_1_array = link_obj_set[link_id].tau_1_array
                omega = stream_instance_obj.omega
                stream_id = stream_instance_obj.stream_id
                # hop_id = stream_instance_obj.hop_id
                size = stream_obj_set[stream_id].size
                speed = link_obj_set[link_id].speed
                trans_duration = math.ceil(size * 8 / speed)
                # trans_duration = \
                #     stream_obj_set[stream_id].route_obj_set[hop_id].trans_duration
                tau_1_array = Store(tau_1_array, omega, tau_1_array[omega] + trans_duration)
                link_obj_set[link_id].tau_1_array = tau_1_array
                hop_id += 1

    # 给tau添加约束
    for link_obj in link_obj_set:
        gcl_len = link_obj.gcl_len
        tau_array = link_obj.tau_array
        tau_0_array = link_obj.tau_0_array
        tau_1_array = link_obj.tau_1_array
        if len(link_obj.stream_array) == 0:
            continue
        for k in range(gcl_len):
            # s.add(tau_array == Store(tau_array, k, tau_0_array[k] + tau_1_array[k]))
            constraint_5 = (tau_array == Store(tau_array, k, tau_0_array[k] + tau_1_array[k]))
            formula.append(constraint_5)
            # s.add(constraint_5)

    # 6.    stream constraint
    #       同一个报文在相邻两跳之间的先后顺序
    for instance_obj_set_per_stream in stream_instance_obj_set:
        route_path_len = len(instance_obj_set_per_stream)
        instance_num_in_hyper_period = len(instance_obj_set_per_stream[0])
        for j in range(instance_num_in_hyper_period):
            for k in range(route_path_len - 1):
                pre_instance_obj = instance_obj_set_per_stream[k][j]
                suc_instance_obj = instance_obj_set_per_stream[k + 1][j]
                pre_link_id = pre_instance_obj.link_id
                suc_link_id = suc_instance_obj.link_id
                pre_tau = link_obj_set[pre_link_id].tau_array
                suc_phi = link_obj_set[suc_link_id].phi_array
                pre_omega = pre_instance_obj.omega
                suc_omega = suc_instance_obj.omega
                constraint_6 = (pre_tau[pre_omega] + sync_precision <= suc_phi[suc_omega])
                formula.append(constraint_6)
                # s.add(constraint_6)

    # print(formula)

    # 7. stream isolation constraint
    # 描述的是在一条链路上汇聚的任意两个帧实例之间的关系
    # loop1：   对于每一条链路，找到属于这一条链路的所有流量的集合，
    #           并记录这些流量在其哪一跳经过该链路，用于索引route[]，
    #           方便找到该流量的上一跳
    for link_obj in link_obj_set:
        # stream_set里面记录的是经过这条链路的流量
        # 其中包含两个参数：stream_id 以及 hop_id
        # hop_id用于索引Stream对象里面的route_path_set数组
        stream_id_and_hop_id_set = link_obj.stream_array
        stream_num = len(stream_id_and_hop_id_set)

        # 当前链路的tau数组
        ab_tau_array = link_obj.tau_array
        # 当前链路的phi数组
        ab_phi_array = link_obj.phi_array
        # 当前链路的kappa数组
        ab_kappa_array = link_obj.kappa_array

        # loop2：   找到任意两条流量
        for i in range(stream_num):
            for j in range(i + 1, stream_num):
                i_stream_id = stream_id_and_hop_id_set[i].stream_id
                j_stream_id = stream_id_and_hop_id_set[j].stream_id

                i_ab_hop_id = stream_id_and_hop_id_set[i].hop_id
                j_ab_hop_id = stream_id_and_hop_id_set[j].hop_id

                # 取得两条流在该链路上的所有报文实例
                i_stream_instance_obj_set_at_ab_hop = stream_instance_obj_set[i_stream_id][i_ab_hop_id]
                j_stream_instance_obj_set_at_ab_hop = stream_instance_obj_set[j_stream_id][j_ab_hop_id]

                # 如果当前链路是起源于talker的链路
                # 这意味着这些流没有上一跳的节点，那么约束就要进行变化
                if i_ab_hop_id == 0 and j_ab_hop_id == 0:
                    # loop3：   找到这两条流量的调度周期内的任意两个报文，添加约束
                    # for k_ab_instance_obj in i_stream_instance_obj_set_at_ab_hop:
                    #     for l_ab_instance_obj in j_stream_instance_obj_set_at_ab_hop:
                    #         i_k_omega = k_ab_instance_obj.omega
                    #         j_l_omega = l_ab_instance_obj.omega
                    #
                    #         constraint_7 = Or(ab_tau_array[i_k_omega] + sync_precision <=
                    #                           ab_phi_array[j_l_omega],
                    #                           ab_tau_array[j_l_omega] + sync_precision <=
                    #                           ab_phi_array[i_k_omega],
                    #                           ab_kappa_array[i_k_omega] != ab_kappa_array[j_l_omega],
                    #                           i_k_omega == j_l_omega)
                    #         formula.append(constraint_7)
                    # s.add(constraint_7)
                    pass

                else:
                    # 如果当前链路不是起源于talker的链路
                    # 这意味着这些流有各自的上一跳节点，因此需要添加四个式子
                    i_xa_hop_id = stream_id_and_hop_id_set[i].hop_id - 1
                    j_ya_hop_id = stream_id_and_hop_id_set[j].hop_id - 1
                    # 取上一跳链路的phi数组
                    # 首先取上一跳链路的link_id
                    # i_xa_link_id = stream_obj_set[i_stream_id].route_obj_set[i_xa_hop_id].link_id
                    # j_ya_link_id = stream_obj_set[j_stream_id].route_obj_set[j_ya_hop_id].link_id
                    i_xa_link_id = stream_obj_set[i_stream_id].route[i_xa_hop_id]
                    j_ya_link_id = stream_obj_set[j_stream_id].route[j_ya_hop_id]
                    # 使用link_id取得phi数组
                    i_xa_hop_phi_array = link_obj_set[i_xa_link_id].phi_array
                    j_ya_hop_phi_array = link_obj_set[j_ya_link_id].phi_array
                    # 取得两条流在其上一跳链路上的所有报文实例
                    i_stream_instance_obj_set_at_xa_hop = stream_instance_obj_set[i_stream_id][i_xa_hop_id]
                    j_stream_instance_obj_set_at_ya_hop = stream_instance_obj_set[j_stream_id][j_ya_hop_id]

                    # loop3：   找到这两条流量的调度周期内的任意两个报文，添加约束
                    for (k_ab_instance_obj, k_xa_instance_obj) in \
                            zip(i_stream_instance_obj_set_at_ab_hop, i_stream_instance_obj_set_at_xa_hop):
                        for (l_ab_instance_obj, l_ya_instance_obj) in \
                                zip(j_stream_instance_obj_set_at_ab_hop, j_stream_instance_obj_set_at_ya_hop):
                            i_k_ab_omega = k_ab_instance_obj.omega
                            j_l_ab_omega = l_ab_instance_obj.omega
                            i_k_xa_omega = k_xa_instance_obj.omega
                            j_l_ya_omega = l_ya_instance_obj.omega

                            constraint_7 = Or(ab_tau_array[i_k_ab_omega] + sync_precision <=
                                              j_ya_hop_phi_array[j_l_ya_omega],
                                              ab_tau_array[j_l_ab_omega] + sync_precision <=
                                              i_xa_hop_phi_array[i_k_xa_omega],
                                              ab_kappa_array[i_k_ab_omega] != ab_kappa_array[j_l_ab_omega],
                                              i_k_ab_omega == j_l_ab_omega)
                            formula.append(constraint_7)
                            # s.add(constraint_7)

    # 8. stream end-to-end latency constraint
    for instance_obj_set_per_stream in stream_instance_obj_set:
        instance_num_in_hyper_period = len(instance_obj_set_per_stream[0])

        first_link_id = instance_obj_set_per_stream[0][0].link_id
        last_link_id = instance_obj_set_per_stream[-1][0].link_id
        stream_id = instance_obj_set_per_stream[0][0].stream_id
        last_tau_array = link_obj_set[last_link_id].tau_array
        first_phi_array = link_obj_set[first_link_id].phi_array
        latency_requirement = stream_obj_set[stream_id].latency_requirement
        for i in range(instance_num_in_hyper_period):
            first_instance_obj = instance_obj_set_per_stream[0][i]
            last_instance_obj = instance_obj_set_per_stream[-1][i]
            first_omega = first_instance_obj.omega
            last_omega = last_instance_obj.omega
            constraint_8 = (last_tau_array[last_omega] - first_phi_array[first_omega] <=
                            latency_requirement - sync_precision)
            formula.append(constraint_8)
            # s.add(constraint_8)

    # 9. stream jitter constraints
    # sender jitter
    for instance_obj_set_per_stream in stream_instance_obj_set:
        instance_obj_set_at_first_link = instance_obj_set_per_stream[0]
        instance_num_in_hyper_period = len(instance_obj_set_at_first_link)

        link_id = instance_obj_set_at_first_link[0].link_id
        phi_array = link_obj_set[link_id].phi_array
        tau_array = link_obj_set[link_id].tau_array

        stream_id = instance_obj_set_at_first_link[0].stream_id
        period = stream_obj_set[stream_id].period
        # trans_duration = stream_obj_set[stream_id].route_obj_set[0].trans_duration
        size = stream_obj_set[stream_id].size
        speed = link_obj_set[link_id].speed
        trans_duration = math.ceil(size * 8 / speed)

        jitter_requirement = stream_obj_set[stream_id].jitter_requirement
        for j in range(instance_num_in_hyper_period):
            for k in range(instance_num_in_hyper_period):
                j_omega = instance_obj_set_at_first_link[j].omega
                k_omega = instance_obj_set_at_first_link[k].omega

                constraint_9 = ((tau_array[j_omega] - j * period) - (phi_array[k_omega] - k * period) -
                                trans_duration <= jitter_requirement)
                formula.append(constraint_9)
                # s.add(constraint_9)

    # receiver jitter
    for instance_obj_set_per_stream in stream_instance_obj_set:
        instance_obj_set_at_last_link = instance_obj_set_per_stream[-1]
        instance_num_in_hyper_period = len(instance_obj_set_at_last_link)

        link_id = instance_obj_set_at_last_link[0].link_id
        phi_array = link_obj_set[link_id].phi_array
        tau_array = link_obj_set[link_id].tau_array

        stream_id = instance_obj_set_at_last_link[0].stream_id
        period = stream_obj_set[stream_id].period
        # trans_duration = stream_obj_set[stream_id].route_obj_set[0].trans_duration
        size = stream_obj_set[stream_id].size
        speed = link_obj_set[link_id].speed
        trans_duration = math.ceil(size * 8 / speed)
        jitter_requirement = stream_obj_set[stream_id].jitter_requirement
        for j in range(instance_num_in_hyper_period):
            for k in range(instance_num_in_hyper_period):
                j_omega = instance_obj_set_at_last_link[j].omega
                k_omega = instance_obj_set_at_last_link[k].omega

                constraint_9 = ((tau_array[j_omega] - j * period) - (phi_array[k_omega] - k * period) -
                                trans_duration <= jitter_requirement)
                formula.append(constraint_9)
    return formula


def _parse_z3_model(model):
    solution = []
    for declare in model.decls():
        name = declare.name()
        value = model[declare]
        solution.append({'name': name, 'value': value})
    return solution


def add_and_solve_constraints(constraint_set,
                              timeout=-1):
    start = 0
    end = 0
    s = Solver()
    if timeout > 0:
        s.set(timeout=timeout)

    for constraint in constraint_set:
        s.add(constraint)

    declare_set = []
    unknown_reason = ''
    # 开始计时
    start = time.time_ns()
    # 判断是否有可行解
    sat_or_not = s.check()
    if sat_or_not == sat:
        model = s.model()
        end = time.time_ns()
        print("start time: %f" % start)
        print("end time: %f" % end)
        # 输出变量声明的集合
        declare_set = _parse_z3_model(model)
    elif sat_or_not == unsat:
        # 输出时间
        end = time.time_ns()
        # 输出一个空的declare_set
    elif sat_or_not == unknown:
        end = time.time_ns()
        # 输出一个空的declare_set
        # 输出unknown的原因
        unknown_reason = s.reason_unknown()
        pass

    time_used_in_second = (end - start) / 1000000000

    print('time_used:')
    print(time_used_in_second)

    print('sat_or_not:')
    print(str(sat_or_not))

    # 返回time_used_in_second、sat_or_not、
    # declare_set、(unknown reason)
    return {'time_used_in_second': time_used_in_second, 'sat_or_not': str(sat_or_not),
            'declare_set': declare_set, 'unknown_reason': unknown_reason}


# 打印表头和phi、tau、kappa的值
def _format_table_header_or_array(fd, name, array, width):
    # width = 9
    length = len(array)
    format_list = ['|', name, '|']
    for item in array:
        format_list.append(str(item))
        format_list.append('|')

    format_str = "{0[0]}{0[1]:^%d}{0[2]}" % width
    index = 3
    for i in range(length):
        format_str = format_str + "{0[%d]:^%d}{0[%d]}" % (index, width, index + 1)
        index += 2

    fd.write(format_str.format(format_list))
    fd.write('\n')

    divider = '|' + '-' * width + '|'
    for i in range(length):
        divider = divider + '-' * width + '|'

    fd.write(divider)
    fd.write('\n')


# 将array的值写入文本文档
def _write_arrays_to_txt(fd, phi_array, tau_array, kappa_array, width):
    # 先打印表头
    table_len = len(phi_array['value'])
    name = 'INDEX'
    value = range(table_len)
    _format_table_header_or_array(fd, name, value, width)
    # 然后依次打印phi tau和kappa
    # name = phi_array['name']
    name = 'phi'
    value = phi_array['value']
    _format_table_header_or_array(fd, name, value, width)
    # name = tau_array['name']
    name = 'tau'
    value = tau_array['value']
    _format_table_header_or_array(fd, name, value, width)
    # name = kappa_array['name']
    name = 'kappa'
    value = kappa_array['value']
    _format_table_header_or_array(fd, name, value, width)


def _classify_declare_set(declare_set, total_link_num):
    tmp_declare_set = [{'phi_array': {'name': '', 'value': ''},
                        'tau_array': {'name': '', 'value': ''},
                        'kappa_array': {'name': '', 'value': ''},
                        'omega_set': []}
                       for i in range(total_link_num)]

    # window_demo的变量分为四类
    # 1. phi_array，命名：P^(link_id)
    # 2. tau_array（还包括两个中间变量tau_0_array，tau_1_array），命名：T^(link_id)
    # 3. kappa_array，命名：K^(link_id)
    # 4. omega，命名：O_stream_id,instance_id^(link_id)
    for declare in declare_set:
        name = declare['name']
        value = declare['value']
        # 解析link_id
        link_id = int(name.split('(')[1].split(')')[0])
        if re.match(r'P\^.', name):
            tmp_declare_set[link_id]['phi_array'] = declare
        elif re.match(r'T\^.', name):
            tmp_declare_set[link_id]['tau_array'] = declare
        elif re.match(r'K\^.', name):
            tmp_declare_set[link_id]['kappa_array'] = declare
        elif re.match(r'O_.', name):
            tmp_declare_set[link_id]['omega_set'].append(declare)
    # print(tmp_declare_set)
    return tmp_declare_set


# 将z3 Array变量转化成可读的列表
# 注意：只转化那些有“有意义”的值，“有意义”是指
# 该位置（index）有数据帧的omega对应
def _transform_z3_array_to_list(array, gcl_len, omega_set):
    # 提取出omega_set的值
    # print(omega_set)
    omega_set = [omega['value'] for omega in omega_set]
    # print(omega_set)
    array_to_list = ['n/a'] * gcl_len
    for i in range(gcl_len):
        if str(i) in omega_set:
            value = str(simplify(array[i]))
            array_to_list[i] = value
    return array_to_list


# 将omega的值按照大小进行排序
def _sort_z3_int_ref(omega_set):
    # 将omega的值由IntSort转化成字符串
    for omega in omega_set:
        omega['value'] = str(omega['value'])
    # 按照omega的值的大小，将经过某条链路的omega进行排序
    omega_set.sort(key=lambda x: x['value'])
    return omega_set


# 将declare_set中的z3变量（Array和Int）转化成
# “可读”的值
def _transform_z3_declare_set_to_readable_declare_set(declare_set,
                                                      link_obj_set):
    link_id = 0
    for declare in declare_set:
        omega_set = declare['omega_set']
        gcl_len = link_obj_set[link_id].gcl_len

        # 如果某条链路没有ST流经过
        # 那么该链路的未知量就不会被添加到z3
        # 因此z3不会输出该链路的未知数
        if not omega_set:
            for array_name in ['phi_array', 'tau_array', 'kappa_array']:
                declare[array_name]['value'] = ['n/a'] * gcl_len
        # 如果某条链路有ST流经过
        elif omega_set:
            for array_name in ['phi_array', 'tau_array', 'kappa_array']:
                array = declare[array_name]['value']
                array_to_list = _transform_z3_array_to_list(array, gcl_len, omega_set)
                declare[array_name]['value'] = array_to_list
            declare['omega_set'] = _sort_z3_int_ref(omega_set)
        link_id += 1
    # print(declare_set)
    return declare_set


# 打印omega
def _write_omega_to_txt(f, omega_set, gcl_len, width):
    width = width + 6
    f.write('stream\'s window index as follow:\n')
    divider_between_array_and_int_str = '-' * (3 * (width + 1) + 1)
    f.write("%s\n" % divider_between_array_and_int_str)

    # 打印表头
    format_str = '{}{:^%d}{}{:^%d}{}{:^%d}{}' % (width, width, width)
    f.write(format_str.format('|', 'stream_id', '|', 'instance_id', '|', 'omega', '|'))
    f.write('\n')
    f.write(format_str.format('|', '-' * width, '|', '-' * width, '|', '-' * width, '|'))
    f.write('\n')

    for omega in omega_set:
        name = omega['name']
        # print(name)
        value = omega['value']
        # omega的命名规则
        # omega，命名：O_stream_id,instance_id^(link_id)
        stream_id = name.split('_')[1].split(',')[0]
        instance_id = name.split(',')[1].split('^')[0]
        f.write(format_str.format('|', stream_id, '|', instance_id, '|', value, '|'))
        f.write('\n')
        f.write(format_str.format('|', '-' * width, '|', '-' * width, '|', '-' * width, '|'))
        f.write('\n')

    f.write("%s\n" % divider_between_array_and_int_str)


def _write_time_used_to_txt(f, time_used_in_second):
    divider = '+' * 80
    f.write('%s\n' % divider)
    f.write('time used:\n')
    f.write("%s s\n" % time_used_in_second)
    f.write("%s min\n" % (time_used_in_second / 60))
    return


def write_declare_set_to_txt(result_set,
                             link_obj_set,
                             solution_txt):
    time_used_in_second = result_set['time_used_in_second']
    sat_or_not = result_set['sat_or_not']
    z3_declare_set = result_set['declare_set']
    unknown_reason = result_set['unknown_reason']

    f = open(solution_txt, 'w')

    # 如果有可行解
    if sat_or_not == 'sat':
        width = 9

        z3_declare_set = _classify_declare_set(z3_declare_set, len(link_obj_set))

        readable_declare_set = \
            _transform_z3_declare_set_to_readable_declare_set(z3_declare_set, link_obj_set)

        link_id = 0
        for declare in readable_declare_set:
            gcl_len = link_obj_set[link_id].gcl_len
            src_node_id = link_obj_set[link_id].src_node
            dst_node_id = link_obj_set[link_id].dst_node

            divider_between_link_str = '=' * ((gcl_len + 1) * (width + 1) + 1)
            f.write("%s\n" % divider_between_link_str)

            src_to_dst = '(%d, %d)' % (src_node_id, dst_node_id)
            f.write('arrays at link %s, link_id: %d\n' % (src_to_dst, link_id))

            '''打印链路上的phi、tau、kappa'''
            _write_arrays_to_txt(f,
                                 declare['phi_array'],
                                 declare['tau_array'],
                                 declare['kappa_array'],
                                 width)

            '''打印该链路上的所有omega'''
            omega_set = declare['omega_set']
            _write_omega_to_txt(f, omega_set, gcl_len, width)

            f.write('\n')

            link_id += 1
    elif sat_or_not == 'unsat':
        f.write('unsat\n')
    elif sat_or_not == 'unknown':
        f.write('unknown\n')
        # 写入原因
        f.write('the reason for unknown result: %s\n' % unknown_reason)

    # 将求解时间写入文件
    _write_time_used_to_txt(f, time_used_in_second)

    f.close()
